(*
Extract the cuts, as permuters |
mark the types, as continuations || 
*)

(*
1. Delimited continuations as series of cuts, Cuts as series of delimited continuations.
2. Cut yields a permuter. Permuter is a set of cuts.
3. Cut yields different outcome (anth, ananth) depending on embedded differentiators.
4. Differentiators are cuts.
5. Each enumeration of a delimited continuation yields a cut.
6. A delimited continuation yields delimited continuation(s), or have its result thrown away.
7. Many delimited continuations can compose to yield a delimited continuation.
8. Enumeration order (induction order) of a delimited continuation is constrained by its ancestor and descendent delimited continuations.
9. Packaging differentiators inside lambda formulas yields varying lengths of proof traces.
10. Metaproof is a set of cuts along with the proper delimited continuations to provide an induction order.
*)

(* Forgetting proof(s) increases time complexity. *)